perm filename MIL.INF[1,JRA] blob sn#005820 filedate 1972-10-11 generic text, type T, neo UTF8
00050	
00100	xεA ↔ ( xεB ∨ xεC ) ;
00200	xεB → ¬ xεC ;
00300	(( xεA ∧ yεA ) → ∃z( zεA ∧ x<z ∧ y<z ) );
00400	 x<y ∧ y<z  → x<z ;
00500	;
00600	;
00700	( zεA → ∃x( xεB ∧ z<x ) ) ∨
00800		∀z( zεA → ∃x( xεC ∧ z<x ) ) ;;